g:GrpSig, x:|g|. e  x 

latex

Up	groups 1
Definitions of Statement	|g|
Definitions	True, T, t  T, x:A. B(x), P  Q, SqStable(P), |g|
Lemmas	grp sig wf, hgrp car wf, grp id wf, sq stable grp leq